perf(ecsm): echo yR and yG, halving the ecalls per ecrecover - #941
Draft
diegokingston wants to merge 11 commits into
Draft
perf(ecsm): echo yR and yG, halving the ecalls per ecrecover#941diegokingston wants to merge 11 commits into
diegokingston wants to merge 11 commits into
Conversation
ecrecover needs the full public key (the address is keccak(X‖Y)), but the ECSM ecall returned only xR. With an x-only k·P oracle that costs FOUR ecalls: one x(k·P) query carries no information about the sign of y, since x(k·P) = x(k·(−P)), so each of the two lincomb terms needs a second query at a shifted scalar to pin it (`solve_y`). Hinting does not help — verifying a sign costs exactly the scalar multiplication it would save. The chip already computes yR (it arrives on the ECDAS bus) and witnesses yG (the yG convolution proves it). Writing both back drops ecrecover to two ecalls, so ~1533 ECDAS rows per signature become ~768 (measured over 2000 random scalars: 383 rows per ecall). yG is echoed, not consumed. The chip may witness EITHER root of xG — the AIR binds only yG² ≡ xG³ + b — so yR alone would be ambiguous: it is ±y(k·P) for the caller's own point. Returning the root used lets the guest resolve it with one comparison, which keeps the root a free choice exactly as spec/ecsm.typ's "Two options for y_G" aside argues, while still handing back a usable y. The alternative (feeding yG IN, as PR #879 does) has to pin the root by a memory read instead, which invalidates that aside, widens the input ABI to 64 bytes and adds an on-curve validation path to the executor. Costs no column: ECSM stays at 667, gaining 8 bus interactions (579 -> 587), i.e. +4 LogUp aux columns. The guest's yR < p check moves from the AIR to the caller's FieldElement::from_bytes, which is free (a CtOption that rejects >= p) and is also what pins yG to a true root: p is odd, so y and p − y differ in parity, but y + p — a second 256-bit representative when y < 2^256 − p ≈ 2^32, and constructible by choosing r — carries the opposite parity. Guest side: solve_y and scalar_near_edge are gone, three batched inversions become one, and k = 1 / k = N−1 stop being degenerate. Operand buffers are now 8-byte aligned so the twelve doubleword accesses take MEMW_A (29 columns + 1 range check) instead of the general path (49 + 8) — the same fix get_hint already carries. Executor: the output buffer is 96 bytes, so its address bound moves from +31 to +95. Reads stay at T and T+1 and writes at T+2 (xR) and T+3 (yR, yG), the free fourth sub-timestamp, so aliasing the output over either input keeps every per-address chain monotone. Verified locally: ECSM AIR constraints hold on generated traces (including k = N−1 and the forged-row rejections), the executor writes and bounds all 96 bytes, and the guest reconstruction matches ProjectivePoint::lincomb under BOTH witnessed roots (an implementation without the fix-up passes the even-root test and fails the odd-root one). The prover suite is unchanged at 390 passed / 167 failed, byte-identical to main: the failures are missing guest ELF artifacts, which this machine cannot build (Apple clang has no RISC-V target). The end-to-end ELF tests and the row-count measurement still need CI / the server. spec/main needs the matching edit: yR and yG become outputs, the write_xR group gains two MEMW groups, and the "Two options for y_G" aside moves from "only x is output" to "the guest resolves the root from the echoed yG".
Collaborator
Author
|
/bench |
|
Benchmark Results for modified programs 🚀
|
Benchmark — real block (
|
| Metric | main | PR | Δ |
|---|---|---|---|
| Peak heap | 47973 MB | 47579 MB | -394 MB (-0.8%) ⚪ |
| Prove time | 136.340s | 134.966s | -1.374s (-1.0%) ⚪ |
✅ No significant change.
Prove-time spread 0.5% (134.997s / 134.966s / 134.331s)
Commit: f714356 · Baseline: cached · Runner: self-hosted bench
`make lint` (the required check) runs `cargo fmt --check --all` and four clippy passes with `-D warnings`. The new `run_ecsm_full` helper tripped both: clippy::type_complexity on its `Result<([u8; 32], [u8; 32], [u8; 32]), _>` return, and then rustfmt on the one-line form the fix produced. Reuse the `ecsm::EcsmOutput` alias the crate already exports for exactly this shape, and re-run rustfmt. `make lint` now exits 0. Also type-checked the riscv64-gated `ecsm_oracle` body on host with a stub ecall (that code is behind `#[cfg(target_arch = "riscv64")]`, so neither `make lint` nor the host tests ever compile it): it builds, both `Align8` buffers come out 8-aligned, and the three 32-byte chunks are extracted in [xR ‖ yR ‖ yG] order. `commit` takes `&[u8]`, so the guest program's `commit(&out.0[..32])` is well-typed. `make test-ethrex-crypto` runs both profiles deliberately (k256 swaps its FieldElement implementation and only asserts magnitudes in debug); 26/26 in each.
diegokingston
marked this pull request as ready for review
August 21, 2026 13:56
diegokingston
marked this pull request as draft
August 21, 2026 14:13
This PR turns yR and yG into values the guest reads and trusts: it reconstructs k*P from yR and resolves the root by comparing the echoed yG against its own y. Both were unforgeable already -- yR through the ECDAS final-receiver tuple, yG through the yG convolution -- but only xR had a test saying so, and the argument that yR is not a free witness lives entirely in a bus tuple's column offsets. Two end-to-end forgery tests, the same shape as the xR one: move the low byte of yR, and of yG, on the single real ECSM row, and the verifier must reject. Two structural tests, because the rest is offsets nothing else checks: - the twelve MEMW writes of [xR || yR || yG], their address offsets (0/32/64 + 8i off ADDR_XR) and their timestamps (xR at T+2, yR and yG at T+3). The aliasing argument is exactly this layout -- the operands are read at T and T+1, so a write moving back onto a read's timestamp would touch one address twice and the memory argument could not prove the chain. T+3 is also the last sub-timestamp of the stride-4 window, so a fourth group has nowhere to go. - the ECDAS tuples: the final receiver's accumulator is (xR, yR), the start sender's is (xG, yG). That is what makes yR the constrained double-and-add output rather than a witness the prover picks. Also fixes collect_ecsm_ops's header comment, which still described the write group as xR at T+2 with no mention of yR/yG at T+3, and adds the cols::yr accessor the xr/xg/yg ones already had.
The doc said "out should be 8-byte aligned so the twelve doubleword accesses land on the aligned memory path (MEMW_A) instead of the general one; the same goes for xg and k". Nothing enforced it, and missing it fails silently -- 49+8 columns per access instead of 29+1, a bigger trace and no other symptom -- which is the worst failure mode to leave to a comment. The wrapper was also copied three times, in ethrex-crypto and in both guest programs. Align8<N> moves to lambda-vm-syscalls next to the ecall it exists for, and ecsm_mul takes &mut Align8<96> / &Align8<32> / &Align8<32>, so the alignment is a type-level guarantee. The three copies collapse into the shared one, and both guest programs now align their xG and k too, which they did not before -- their eight operand reads move to MEMW_A as well.
The executor writes scalar_mul_full's bytes into guest memory and the prover writes the witness columns; the MEMW bus asserts the two are the same claim. Publishing yR and yG put two more values under that coupling, and the two sides compute them differently -- the executor through k256's affine scalar multiplication, the witness through its own double-and-add replay. A disagreement on a sign or a representative would surface only as an unbalanced bus, on whichever scalar happened to hit it. Assert the equality directly over k = 1, 5, 0xABCDEF, (N-1)/2 and N-1, including that both sides lift xG to its even root.
yR and yG are published to guest memory now, and the guest resolves the root by
comparing the echoed yG against the y of its own base point. The byte range
checks bound them only by 2^256, and the quotient columns absorb a multiple of
p, so a prover could publish y + p: a second 256-bit representative, available
whenever y < 2^256 - p (about 2^32). It agrees mod p and carries the OPPOSITE
parity -- which is the bit the caller reads.
Such points are constructible rather than hypothetical: p = 1 mod 3, so cubing
is 3-to-1 and about a third of small y have a curve x.
The PR closed this caller-side, with the CtOption from k256's
FieldElement::from_bytes rejecting >= p inside ecsm_oracle. That works, but it
puts the guarantee in a function that is #[cfg(target_arch = "riscv64")] -- no
host test compiles it, and the unit tests cannot reach it, since FieldElement
cannot represent a non-canonical value to feed it. Two chip-side range checks
give the same guarantee where the rest of the chip's guarantees live, and the
parse stays as a free second line.
xR already had exactly this (XR_SUB_P / OverflowKind::XrLtP), so yR and yG reuse
the machinery unchanged:
- YR_SUB_P and YG_SUB_P, 16 halfwords each. 667 -> 699 columns
- OverflowKind::YrLtP / YgLtP, 7 carry bits + overflow-required each.
413 -> 429 constraints
- 32 IsHalfword sends, with the matching receives in
collect_bitwise_from_ecsm -- the multiplicity has to move with the sends or
the bus does not balance
- y_r_sub_p / y_g_sub_p on the witness
Cost is one row per ecall, so this is 32 cells and 16 constraint evaluations per
ECSM call, against ECDAS's ~383 rows for the same call.
What it buys, beyond not depending on an untested parse: the two caller
assumptions the spec branch introduces mostly go away. ECSM-A2 ("reduce yR
modulo p before use") is gone -- the chip does it. The load-bearing half of
ECSM-A1 is gone too: the comparison no longer has to be made modulo p, because
there is only one representative. What remains of A1 is the design's own
requirement, that the caller compare the root and decline when it matches
neither y nor -y.
spec/ecsm-echo-yg (d4e6c12) needs the matching edit: two constraint groups in
spec/src/ecsm.toml, and the "No such check is made on yR, deliberately"
paragraph plus the assumptions table rewritten to match.
Collaborator
|
/ai-review |
Codex Code ReviewNo actionable issues found in the PR diff. |
![claude[bot]](https://avatars.githubusercontent.com/in/1236702?s=60&v=4){kind=small}
| /// the helper above, so a missing replay shows up here rather than as a | ||
| /// mis-sized trace under Disk storage. | ||
| #[test] | ||
| fn count_table_lengths_matches_nonempty_ecsm_trace() { |
Contributor
There was a problem hiding this comment.
Medium — this test should fail as written, and the gap behind it is real.
count_table_lengths (trace_builder.rs:3776) has branches for ecall_commit and ecall_hint but none for ecall_ecsm, so it replays none of the 23 MEMW ops collect_ecsm_ops emits per call. For test_ecsm.s (sp is 8-aligned, so every ECSM doubleword takes the Aligned route):
memw_aligned: predicted ≈ 8 (thesdstores) → padded 8; actual ≈ 8 + 20 (4 xG + 4 k + 12 output) → padded 32.memw_register: predicted omits the three ECSM register reads (x10/x11/x12).
Both are assert_eq! exact-match tables in assert_count_table_lengths_matches, so the assertion can't hold. (The prover suite couldn't run locally per the PR description — this is in the asm-artifact-dependent set.)
The underlying bug is pre-existing but this PR triples the write side (4 → 12 doublewords per ecall), so the under-estimate feeding auto_storage::decide gets ~3× worse on ecrecover-heavy workloads — that's the path that picks in-memory when disk was needed. Suggest adding the ecall_ecsm branch that mirrors the ecall_hint one (call collect_ecsm_ops and partition_memw over its result) rather than landing a test that documents the omission.
AI ReviewPR #941 · 20 changed files Findings
Status column reflects the verdict from the verifier: deepseek-verifier (openrouter/deepseek/deepseek-v4-pro). AI-001: count_table_lengths ignores ECSM ecalls
Claim The disk-spill sizing helper count_table_lengths handles ecall_commit and ecall_hint but has no branch for cpu_op.ecall_ecsm. Because each ECSM call emits 23 MEMW records (3 register reads + 8 operand reads + 12 output writes), the predicted MEMW/MEMW_A/MEMW_R/LT row counts are too low. The newly added count_table_lengths_matches_nonempty_ecsm_trace test will fail, and disk-spill traces containing ECSM calls may be sized incorrectly. Evidence trace_builder.rs: Suggested fix Add an AI-006: ECSM module doc still describes old 32-byte output
Claim The module-level docstring says the ECSM chip enforces 0 < k < N and xR < p and writes xR back, but the PR extends the output to 96 bytes and adds OverflowKind::YrLtP/YgLtP range checks. Evidence Lines 5-6 of prover/src/tables/ecsm.rs describe the old behavior. Lines 549-567 and 694-695 show the new yR/yG checks, and lines 460-485 show the 12 doubleword writes for [xR‖yR‖yG]. Suggested fix Update the docstring to state that the chip also range-checks yR < p and yG < p and writes back the full 96-byte [xR‖yR‖yG] buffer. Reviewer Lanes
Verification Lanes
Native Codex and Claude reviews run separately and post their own comments. They are not included in this structured provenance report. Discarded candidates (4) — rejected by the verifier
Raw lane outputs, candidates, final issues, and model metrics are uploaded as workflow artifacts. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
ecrecover needs the full public key (the address is keccak(X‖Y)), but the ECSM ecall returned only xR. With an x-only k·P oracle that costs FOUR ecalls: one x(k·P) query carries no information about the sign of y, since x(k·P) = x(k·(−P)), so each of the two lincomb terms needs a second query at a shifted scalar to pin it (
solve_y). Hinting does not help — verifying a sign costs exactly the scalar multiplication it would save.The chip already computes yR (it arrives on the ECDAS bus) and witnesses yG (the yG convolution proves it). Writing both back drops ecrecover to two ecalls, so ~1533 ECDAS rows per signature become ~768 (measured over 2000 random scalars: 383 rows per ecall).
yG is echoed, not consumed. The chip may witness EITHER root of xG — the AIR binds only yG² ≡ xG³ + b — so yR alone would be ambiguous: it is ±y(k·P) for the caller's own point. Returning the root used lets the guest resolve it with one comparison, which keeps the root a free choice exactly as spec/ecsm.typ's "Two options for y_G" aside argues, while still handing back a usable y. The alternative (feeding yG IN, as PR #879 does) has to pin the root by a memory read instead, which invalidates that aside, widens the input ABI to 64 bytes and adds an on-curve validation path to the executor.
Costs no column: ECSM stays at 667, gaining 8 bus interactions (579 -> 587), i.e. +4 LogUp aux columns. The guest's yR < p check moves from the AIR to the caller's FieldElement::from_bytes, which is free (a CtOption that rejects >= p) and is also what pins yG to a true root: p is odd, so y and p − y differ in parity, but y + p — a second 256-bit representative when y < 2^256 − p ≈ 2^32, and constructible by choosing r — carries the opposite parity.
Guest side: solve_y and scalar_near_edge are gone, three batched inversions become one, and k = 1 / k = N−1 stop being degenerate. Operand buffers are now 8-byte aligned so the twelve doubleword accesses take MEMW_A (29 columns + 1 range check) instead of the general path (49 + 8) — the same fix get_hint already carries.
Executor: the output buffer is 96 bytes, so its address bound moves from +31 to +95. Reads stay at T and T+1 and writes at T+2 (xR) and T+3 (yR, yG), the free fourth sub-timestamp, so aliasing the output over either input keeps every per-address chain monotone.
Verified locally: ECSM AIR constraints hold on generated traces (including k = N−1 and the forged-row rejections), the executor writes and bounds all 96 bytes, and the guest reconstruction matches ProjectivePoint::lincomb under BOTH witnessed roots (an implementation without the fix-up passes the even-root test and fails the odd-root one). The prover suite is unchanged at 390 passed / 167 failed, byte-identical to main: the failures are missing guest ELF artifacts, which this machine cannot build (Apple clang has no RISC-V target). The end-to-end ELF tests and the row-count measurement still need CI / the server.
spec/main needs the matching edit: yR and yG become outputs, the write_xR group gains two MEMW groups, and the "Two options for y_G" aside moves from "only x is output" to "the guest resolves the root from the echoed yG".